let AS be AffinSpace; :: thesis: for a, b being Element of AS
for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is being_line
let a, b be Element of AS; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is being_line
let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b implies X /\ Y is being_line )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: ( a in X & b in X ) and
A4: ( a in Y & b in Y ) and
A5: X <> Y and
A6: a <> b ; :: thesis: X /\ Y is being_line
set Z = X /\ Y;
set Q = Line (a,b);
A7: Line (a,b) c= X by A1, A3, A6, Th19;
A8: Line (a,b) c= Y by A2, A4, A6, Th19;
A9: Line (a,b) is being_line by A6, AFF_1:def 3;
A10: X /\ Y c= Line (a,b)
proof
assume not X /\ Y c= Line (a,b) ; :: thesis: contradiction
then consider x being object such that
A11: x in X /\ Y and
A12: not x in Line (a,b) ;
reconsider a9 = x as Element of AS by A11;
A13: x in Y by A11, XBOOLE_0:def 4;
A14: x in X by A11, XBOOLE_0:def 4;
for y being object holds
( y in X iff y in Y )
proof
let y be object ; :: thesis: ( y in X iff y in Y )
A15: now :: thesis: ( y in Y implies y in X )
assume A16: y in Y ; :: thesis: y in X
now :: thesis: ( y <> x implies y in X )
reconsider b9 = y as Element of AS by A16;
set M = Line (a9,b9);
A17: a9 in Line (a9,b9) by AFF_1:15;
A18: b9 in Line (a9,b9) by AFF_1:15;
assume A19: y <> x ; :: thesis: y in X
then A20: Line (a9,b9) is being_line by AFF_1:def 3;
A21: Line (a9,b9) c= Y by A2, A13, A16, A19, Th19;
A22: now :: thesis: ( not Line (a9,b9) // Line (a,b) implies y in X )
assume not Line (a9,b9) // Line (a,b) ; :: thesis: y in X
then consider q being Element of AS such that
A23: q in Line (a9,b9) and
A24: q in Line (a,b) by A2, A9, A8, A20, A21, Th22;
Line (a9,b9) = Line (a9,q) by A12, A20, A17, A23, A24, AFF_1:57;
then Line (a9,b9) c= X by A1, A7, A12, A14, A24, Th19;
hence y in X by A18; :: thesis: verum
end;
now :: thesis: ( Line (a9,b9) // Line (a,b) implies y in X )
assume Line (a9,b9) // Line (a,b) ; :: thesis: y in X
then Line (a9,b9) c= X by A1, A7, A14, A17, Th23;
hence y in X by A18; :: thesis: verum
end;
hence y in X by A22; :: thesis: verum
end;
hence y in X by A11, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: ( y in X implies y in Y )
assume A25: y in X ; :: thesis: y in Y
now :: thesis: ( y <> x implies y in Y )
reconsider b9 = y as Element of AS by A25;
set M = Line (a9,b9);
A26: a9 in Line (a9,b9) by AFF_1:15;
A27: b9 in Line (a9,b9) by AFF_1:15;
assume A28: y <> x ; :: thesis: y in Y
then A29: Line (a9,b9) is being_line by AFF_1:def 3;
A30: Line (a9,b9) c= X by A1, A14, A25, A28, Th19;
A31: now :: thesis: ( not Line (a9,b9) // Line (a,b) implies y in Y )
assume not Line (a9,b9) // Line (a,b) ; :: thesis: y in Y
then consider q being Element of AS such that
A32: q in Line (a9,b9) and
A33: q in Line (a,b) by A1, A9, A7, A29, A30, Th22;
Line (a9,b9) = Line (a9,q) by A12, A29, A26, A32, A33, AFF_1:57;
then Line (a9,b9) c= Y by A2, A8, A12, A13, A33, Th19;
hence y in Y by A27; :: thesis: verum
end;
now :: thesis: ( Line (a9,b9) // Line (a,b) implies y in Y )
assume Line (a9,b9) // Line (a,b) ; :: thesis: y in Y
then Line (a9,b9) c= Y by A2, A8, A13, A26, Th23;
hence y in Y by A27; :: thesis: verum
end;
hence y in Y by A31; :: thesis: verum
end;
hence y in Y by A11, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( y in X iff y in Y ) by A15; :: thesis: verum
end;
hence contradiction by A5, TARSKI:2; :: thesis: verum
end;
Line (a,b) c= X /\ Y by A7, A8, XBOOLE_1:19;
hence X /\ Y is being_line by A9, A10, XBOOLE_0:def 10; :: thesis: verum