:: DIRAF semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be non empty set ;
let R be Relation of [:X,X:];
func lambda R -> Relation of [:X,X:] means :Def1: :: DIRAF:def 1
for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in it iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) );
existence
ex b1 being Relation of [:X,X:] st
for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) )
proof end;
uniqueness
for b1, b2 being Relation of [:X,X:] st ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) & ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b2 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines lambda DIRAF:def 1 :
for X being non empty set
for R, b3 being Relation of [:X,X:] holds
( b3 = lambda R iff for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b3 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) );

definition
let S be non empty AffinStruct ;
func Lambda S -> strict AffinStruct equals :: DIRAF:def 2
AffinStruct(# the carrier of S,(lambda the CONGR of S) #);
correctness
coherence
AffinStruct(# the carrier of S,(lambda the CONGR of S) #) is strict AffinStruct
;
;
end;

:: deftheorem defines Lambda DIRAF:def 2 :
for S being non empty AffinStruct holds Lambda S = AffinStruct(# the carrier of S,(lambda the CONGR of S) #);

registration
let S be non empty AffinStruct ;
cluster Lambda S -> non empty strict ;
coherence
not Lambda S is empty
proof end;
end;

theorem :: DIRAF:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRAF:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRAF:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: DIRAF:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S holds x,y // x,y
proof end;

Lm1: for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
z,t // x,y
proof end;

theorem Th5: :: DIRAF:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
( y,x // t,z & z,t // x,y & t,z // y,x )
proof end;

theorem Th6: :: DIRAF:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for z, t, x, y, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds
x,y // u,w
proof end;

theorem Th7: :: DIRAF:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S holds
( x,x // y,z & y,z // x,x )
proof end;

theorem Th8: :: DIRAF:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t & x,y // t,z & not x = y holds
z = t
proof end;

theorem Th9: :: DIRAF:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred Mid a,b,c means :Def3: :: DIRAF:def 3
a,b // b,c;
end;

:: deftheorem Def3 defines Mid DIRAF:def 3 :
for S being non empty AffinStruct
for a, b, c being Element of S holds
( Mid a,b,c iff a,b // b,c );

theorem :: DIRAF:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: DIRAF:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) )
proof end;

theorem Th12: :: DIRAF:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b being Element of S st Mid a,b,a holds
a = b
proof end;

theorem :: DIRAF:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
Mid c,b,a
proof end;

theorem :: DIRAF:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S holds
( Mid x,x,y & Mid x,y,y )
proof end;

theorem :: DIRAF:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, c, d being Element of S st Mid a,b,c & Mid a,c,d holds
Mid b,c,d
proof end;

theorem :: DIRAF:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d
proof end;

theorem Th17: :: DIRAF:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S ex z being Element of S st
( Mid x,y,z & y <> z )
proof end;

theorem :: DIRAF:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds
x = y
proof end;

theorem :: DIRAF:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid y,z,t holds
Mid y,t,z
proof end;

theorem :: DIRAF:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & Mid x,y,z & Mid x,y,t & not Mid x,z,t holds
Mid x,t,z
proof end;

theorem :: DIRAF:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, t, z being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds
Mid x,z,y
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c, d be Element of S;
pred a,b '||' c,d means :Def4: :: DIRAF:def 4
( a,b // c,d or a,b // d,c );
end;

:: deftheorem Def4 defines '||' DIRAF:def 4 :
for S being non empty AffinStruct
for a, b, c, d being Element of S holds
( a,b '||' c,d iff ( a,b // c,d or a,b // d,c ) );

theorem :: DIRAF:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRAF:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, c, d being Element of S holds
( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )
proof end;

theorem Th24: :: DIRAF:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S holds
( x,y '||' y,x & x,y '||' x,y )
proof end;

theorem Th25: :: DIRAF:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y '||' z,z & z,z '||' x,y )
proof end;

Lm2: for S being OAffinSpace
for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds
z,t '||' u,w
proof end;

theorem Th26: :: DIRAF:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S st x,y '||' x,z holds
y,x '||' y,z
proof end;

theorem Th27: :: DIRAF:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x,y '||' z,t holds
( x,y '||' t,z & y,x '||' z,t & y,x '||' t,z & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x )
proof end;

theorem Th28: :: DIRAF:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, x, y, z, t being Element of S st a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) holds
x,y '||' z,t
proof end;

theorem Th29: :: DIRAF:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y '||' x,z
proof end;

theorem Th30: :: DIRAF:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, z, y being Element of S ex t being Element of S st
( x,z '||' y,t & y <> t )
proof end;

theorem Th31: :: DIRAF:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S ex t being Element of S st
( x,y '||' z,t & x,z '||' y,t )
proof end;

theorem Th32: :: DIRAF:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for z, x, t, y being Element of S st z,x '||' x,t & x <> z holds
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred LIN a,b,c means :Def5: :: DIRAF:def 5
a,b '||' a,c;
end;

:: deftheorem Def5 defines LIN DIRAF:def 5 :
for S being non empty AffinStruct
for a, b, c being Element of S holds
( LIN a,b,c iff a,b '||' a,c );

notation
let S be non empty AffinStruct ;
let a, b, c be Element of S;
synonym a,b,c is_collinear for LIN a,b,c;
end;

theorem :: DIRAF:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRAF:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
a,b,c is_collinear
proof end;

theorem :: DIRAF:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for a, b, c being Element of S holds
( not a,b,c is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b )
proof end;

Lm3: for S being OAffinSpace
for x, y, z being Element of S st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear )
proof end;

theorem Th36: :: DIRAF:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z being Element of S st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear )
proof end;

theorem Th37: :: DIRAF:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S holds
( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear )
proof end;

theorem Th38: :: DIRAF:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t, u being Element of S st x <> y & x,y,z is_collinear & x,y,t is_collinear & x,y,u is_collinear holds
z,t,u is_collinear
proof end;

theorem :: DIRAF:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & x,y,z is_collinear & x,y '||' z,t holds
x,y,t is_collinear
proof end;

theorem :: DIRAF:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds
x,y '||' z,t
proof end;

theorem :: DIRAF:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for u, z, x, y, w being Element of S st u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear holds
x,y,w is_collinear
proof end;

theorem Th42: :: DIRAF:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y,z is_collinear
proof end;

theorem :: DIRAF:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for x, y being Element of S st x <> y holds
ex z being Element of S st not x,y,z is_collinear
proof end;

theorem :: DIRAF:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th45: :: DIRAF:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for AS being non empty AffinStruct st AS = Lambda S holds
for a, b, c, d being Element of S
for a', b', c', d' being Element of AS st a = a' & b = b' & c = c' & d = d' holds
( a',b' // c',d' iff a,b '||' c,d )
proof end;

theorem Th46: :: DIRAF:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace
for AS being non empty AffinStruct st AS = Lambda S holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )
proof end;

definition
let IT be non empty AffinStruct ;
canceled;
attr IT is AffinSpace-like means :Def7: :: DIRAF:def 7
( ( for x, y, z, t, u, w being Element of IT holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds
ex u being Element of IT st
( y,x // x,u & y,z // t,u ) ) );
end;

:: deftheorem DIRAF:def 6 :
canceled;

:: deftheorem Def7 defines AffinSpace-like DIRAF:def 7 :
for IT being non empty AffinStruct holds
( IT is AffinSpace-like iff ( ( for x, y, z, t, u, w being Element of IT holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds
ex u being Element of IT st
( y,x // x,u & y,z // t,u ) ) ) );

registration
cluster non empty non trivial strict AffinSpace-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is AffinSpace-like )
proof end;
end;

definition
mode AffinSpace is non empty non trivial AffinSpace-like AffinStruct ;
end;

theorem :: DIRAF:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being AffinSpace holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) by Def7, REALSET2:def 7;

theorem Th48: :: DIRAF:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinSpace holds Lambda S is AffinSpace
proof end;

theorem :: DIRAF:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being non empty AffinStruct holds
( ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) iff AS is AffinSpace ) by Def7, REALSET2:def 7;

theorem Th50: :: DIRAF:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinPlane
for x, y, z, t being Element of S st not x,y '||' z,t holds
ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u )
proof end;

theorem Th51: :: DIRAF:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being non empty AffinStruct
for S being OAffinPlane st AS = Lambda S holds
for x, y, z, t being Element of AS st not x,y // z,t holds
ex u being Element of AS st
( x,y // x,u & z,t // z,u )
proof end;

definition
let IT be non empty AffinStruct ;
attr IT is 2-dimensional means :Def8: :: DIRAF:def 8
for x, y, z, t being Element of IT st not x,y // z,t holds
ex u being Element of IT st
( x,y // x,u & z,t // z,u );
end;

:: deftheorem Def8 defines 2-dimensional DIRAF:def 8 :
for IT being non empty AffinStruct holds
( IT is 2-dimensional iff for x, y, z, t being Element of IT st not x,y // z,t holds
ex u being Element of IT st
( x,y // x,u & z,t // z,u ) );

registration
cluster strict 2-dimensional AffinStruct ;
existence
ex b1 being AffinSpace st
( b1 is strict & b1 is 2-dimensional )
proof end;
end;

definition
mode AffinPlane is 2-dimensional AffinSpace;
end;

theorem :: DIRAF:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DIRAF:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OAffinPlane holds Lambda S is AffinPlane
proof end;

theorem :: DIRAF:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being non empty AffinStruct holds
( AS is AffinPlane iff ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) & ( for x, y, z, t being Element of AS st not x,y // z,t holds
ex u being Element of AS st
( x,y // x,u & z,t // z,u ) ) ) ) by Def7, Def8, REALSET2:def 7;