set X = Af MOS;
Af MOS is OrdTrapSpace-like

proof

let a, b, c, d, a1, b1, c1, d1, p, q be Element of (Af MOS); :: according to GEOMTRAP:def 14 :: thesis: ( ( a,b // b,c implies ( a = b & b = c ) ) & ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of (Af MOS) st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )
reconsider a' = a, b' = b, c' = c, d' = d, a1' = a1, b1' = b1, c1' = c1, d1' = d1, p' = p, q' = q as Element of MOS ;

A1: now

let a, b, c, d be Element of (Af MOS); :: thesis: for a', b', c', d' being Element of the carrier of MOS st a = a' & b = b' & c = c' & d = d' holds
( ( a,b // c,d implies a',b' // c',d' ) & ( a',b' // c',d' implies a,b // c,d ) )
let a', b', c', d' be Element of the carrier of MOS; :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( ( a,b // c,d implies a',b' // c',d' ) & ( a',b' // c',d' implies a,b // c,d ) ) )
assume A2: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis: ( ( a,b // c,d implies a',b' // c',d' ) & ( a',b' // c',d' implies a,b // c,d ) )

hereby :: thesis: ( a',b' // c',d' implies a,b // c,d )

assume a,b // c,d ; :: thesis: a',b' // c',d'
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a',b' // c',d' by A2, ANALOAF:def 2; :: thesis: verum

end;

assume a',b' // c',d' ; :: thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of MOS by A2, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: verum

end;

hereby :: thesis: ( ( a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 ) & ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of (Af MOS) st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )

assume a,b // b,c ; :: thesis: ( a = b & b = c )
then a',b' // b',c' by A1;
hence ( a = b & b = c ) by Def13; :: thesis: verum

end;

hereby :: thesis: ( ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of (Af MOS) st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )

assume that
A3: ( a,b // a1,b1 & a,b // c1,d1 ) and
A4: a <> b ; :: thesis: a1,b1 // c1,d1
( a',b' // a1',b1' & a',b' // c1',d1' ) by A1, A3;
then a1',b1' // c1',d1' by A4, Def13;
hence a1,b1 // c1,d1 by A1; :: thesis: verum

end;

hereby :: thesis: ( ex d being Element of (Af MOS) st
( a,b // c,d or a,b // d,c ) & ( a,b // c,p & a,b // c,q & not a = b implies p = q ) )

assume a,b // c,d ; :: thesis: ( c,d // a,b & b,a // d,c )
then a',b' // c',d' by A1;
then ( c',d' // a',b' & b',a' // d',c' ) by Def13;
hence ( c,d // a,b & b,a // d,c ) by A1; :: thesis: verum

end;

thus ex d being Element of (Af MOS) st
( a,b // c,d or a,b // d,c ) :: thesis: ( a,b // c,p & a,b // c,q & not a = b implies p = q )

proof

consider x' being Element of MOS such that
A5: ( a',b' // c',x' or a',b' // x',c' ) by Def13;
reconsider x = x' as Element of (Af MOS) ;
take x ; :: thesis: ( a,b // c,x or a,b // x,c )
thus ( a,b // c,x or a,b // x,c ) by A1, A5; :: thesis: verum

end;

assume ( a,b // c,p & a,b // c,q ) ; :: thesis: ( a = b or p = q )
then ( a',b' // c',p' & a',b' // c',q' ) by A1;
hence ( a = b or p = q ) by Def13; :: thesis: verum

end;

hence Af MOS is OrdTrapSpace-like ; :: thesis: verum