set X = AffinStruct(# the carrier of MOS, the CONGR of MOS #);
now :: thesis: 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,d1
let p, q, a, a1, b, b1, c, c1, d, d1 be Element of AffinStruct(# the carrier of MOS, the CONGR of MOS #); :: 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
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 ; :: thesis: 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 MOS ;
A5: now :: thesis: 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 #); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( ( a,b // c,d implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies a,b // c,d ) )
hereby :: thesis: ( a9,b9 // c9,d9 implies a,b // c,d )
assume a,b // c,d ; :: thesis: a9,b9 // c9,d9
then [[a,b],[c,d]] in the CONGR of MOS by ANALOAF:def 2;
hence a9,b9 // c9,d9 by A6, ANALOAF:def 2; :: thesis: verum
end;
assume a9,b9 // c9,d9 ; :: thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of MOS by A6, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: 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; :: thesis: verum
end;
hence AffinStruct(# the carrier of MOS, the CONGR of MOS #) is Regular ; :: thesis: verum