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