consider MOTS being MidOrdTrapSpace;
set X = Af MOTS;

A1: now

let a, b, c, d be Element of ; :: thesis: for a', b', c', d' being Element of the carrier of MOTS 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 MOTS; :: 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 MOTS 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 MOTS by A2, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: verum

end;

Af MOTS is Regular

proof

let p, q, a, a1, b, b1, c, c1, d, d1 be Element of ; :: according to GEOMTRAP:def 16 :: thesis: ( p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d implies a1,b1 // c1,d1 )
assume that
A3: p <> q and
A4: ( p,q // a,a1 & p,q // b,b1 ) and
A5: ( p,q // c,c1 & p,q // d,d1 ) and
A6: a,b // c,d ; :: thesis: a1,b1 // c1,d1
reconsider a' = a, b' = b, c' = c, d' = d, a1' = a1, b1' = b1, c1' = c1, d1' = d1, p' = p, q' = q as Element of ;
A7: ( p',q' // c',c1' & p',q' // d',d1' ) by A1, A5;
A8: a',b' // c',d' by A1, A6;
( p',q' // a',a1' & p',q' // b',b1' ) by A1, A4;
then a1',b1' // c1',d1' by A3, A7, A8, Def13;
hence a1,b1 // c1,d1 by A1; :: thesis: verum

end;

hence ex b₁ being non empty OrdTrapSpace st
( b₁ is strict & b₁ is Regular ) ; :: thesis: verum