set MOTS = the MidOrdTrapSpace;
set X = AffinStruct(# the carrier of the MidOrdTrapSpace, the CONGR of the MidOrdTrapSpace #);
A1:
now for a, b, c, d being Element of AffinStruct(# the carrier of the MidOrdTrapSpace, the CONGR of the MidOrdTrapSpace #)
for a9, b9, c9, d9 being Element of the carrier of the MidOrdTrapSpace st a = a9 & b = b9 & c = c9 & d = d9 holds
( ( a,b // c,d implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies a,b // c,d ) )let a,
b,
c,
d be
Element of
AffinStruct(# the
carrier of the
MidOrdTrapSpace, the
CONGR of the
MidOrdTrapSpace #);
for a9, b9, c9, d9 being Element of the carrier of the MidOrdTrapSpace st a = a9 & b = b9 & c = c9 & d = d9 holds
( ( a,b // c,d implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies a,b // c,d ) )let a9,
b9,
c9,
d9 be
Element of the
carrier of the
MidOrdTrapSpace;
( a = a9 & b = b9 & c = c9 & d = d9 implies ( ( a,b // c,d implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies a,b // c,d ) ) )assume A2:
(
a = a9 &
b = b9 &
c = c9 &
d = d9 )
;
( ( a,b // c,d implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies a,b // c,d ) )hereby ( a9,b9 // c9,d9 implies a,b // c,d )
assume
a,
b // c,
d
;
a9,b9 // c9,d9then
[[a,b],[c,d]] in the
CONGR of the
MidOrdTrapSpace
by ANALOAF:def 2;
hence
a9,
b9 // c9,
d9
by A2, ANALOAF:def 2;
verum
end; assume
a9,
b9 // c9,
d9
;
a,b // c,dthen
[[a,b],[c,d]] in the
CONGR of the
MidOrdTrapSpace
by A2, ANALOAF:def 2;
hence
a,
b // c,
d
by ANALOAF:def 2;
verum end;
AffinStruct(# the carrier of the MidOrdTrapSpace, the CONGR of the MidOrdTrapSpace #) is Regular
proof
let p,
q,
a,
a1,
b,
b1,
c,
c1,
d,
d1 be
Element of
AffinStruct(# the
carrier of the
MidOrdTrapSpace, the
CONGR of the
MidOrdTrapSpace #);
GEOMTRAP:def 15 ( 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
;
a1,b1 // c1,d1
reconsider a9 =
a,
b9 =
b,
c9 =
c,
d9 =
d,
a19 =
a1,
b19 =
b1,
c19 =
c1,
d19 =
d1,
p9 =
p,
q9 =
q as
Element of the
MidOrdTrapSpace ;
A7:
(
p9,
q9 // c9,
c19 &
p9,
q9 // d9,
d19 )
by A1, A5;
A8:
a9,
b9 // c9,
d9
by A1, A6;
(
p9,
q9 // a9,
a19 &
p9,
q9 // b9,
b19 )
by A1, A4;
then
a19,
b19 // c19,
d19
by A3, A7, A8, Def11;
hence
a1,
b1 // c1,
d1
by A1;
verum
end;
hence
ex b1 being OrdTrapSpace st
( b1 is strict & b1 is Regular )
; verum