set X = AffinStruct(# the carrier of MOS, the CONGR of MOS #);
AffinStruct(# the carrier of MOS, the CONGR of MOS #) is OrdTrapSpace-like
proof
let a, b, c, d, a1, b1, c1, d1, p, q be Element of AffinStruct(# the carrier of MOS, the CONGR of MOS #); :: according to GEOMTRAP:def 13 :: 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 AffinStruct(# the carrier of MOS, the CONGR of 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 a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of MOS ;
A1: 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 A2: ( 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 A2, 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 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 AffinStruct(# the carrier of MOS, the CONGR of 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 a9,b9 // b9,c9 by A1;
hence ( a = b & b = c ) by Def11; :: thesis: verum
end;
hereby :: thesis: ( ( a,b // c,d implies ( c,d // a,b & b,a // d,c ) ) & ex d being Element of AffinStruct(# the carrier of MOS, the CONGR of 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
( a9,b9 // a19,b19 & a9,b9 // c19,d19 ) by A1, A3;
then a19,b19 // c19,d19 by A4, Def11;
hence a1,b1 // c1,d1 by A1; :: thesis: verum
end;
hereby :: thesis: ( ex d being Element of AffinStruct(# the carrier of MOS, the CONGR of 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 a9,b9 // c9,d9 by A1;
then ( c9,d9 // a9,b9 & b9,a9 // d9,c9 ) by Def11;
hence ( c,d // a,b & b,a // d,c ) by A1; :: thesis: verum
end;
thus ex d being Element of AffinStruct(# the carrier of MOS, the CONGR of 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 x9 being Element of MOS such that
A5: ( a9,b9 // c9,x9 or a9,b9 // x9,c9 ) by Def11;
reconsider x = x9 as Element of AffinStruct(# the carrier of MOS, the CONGR of 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 ( a9,b9 // c9,p9 & a9,b9 // c9,q9 ) by A1;
hence ( a = b or p = q ) by Def11; :: thesis: verum
end;
hence AffinStruct(# the carrier of MOS, the CONGR of MOS #) is OrdTrapSpace-like ; :: thesis: verum