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)

hence X /\ Y is being_line by A9, A10, XBOOLE_0:def 10; :: thesis: verum

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

Line (a,b) c= X /\ Y
by A7, A8, XBOOLE_1:19;
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 )

end;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

hence
contradiction
by A5, TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in X iff y in Y )

end;A15: now :: thesis: ( y in Y implies y in X )

assume A16:
y in Y
; :: thesis: y in X

end;now :: thesis: ( y <> x implies y in X )

hence
y in X
by A11, XBOOLE_0:def 4; :: thesis: verumreconsider 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;

end;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;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

now :: thesis: ( Line (a9,b9) // Line (a,b) implies y in X )

hence
y in X
by A22; :: thesis: verumassume
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;then Line (a9,b9) c= X by A1, A7, A14, A17, Th23;

hence y in X by A18; :: thesis: verum

now :: thesis: ( y in X implies y in Y )

hence
( y in X iff y in Y )
by A15; :: thesis: verumassume A25:
y in X
; :: thesis: y in Y

end;now :: thesis: ( y <> x implies y in Y )

hence
y in Y
by A11, XBOOLE_0:def 4; :: thesis: verumreconsider 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;

end;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;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

now :: thesis: ( Line (a9,b9) // Line (a,b) implies y in Y )

hence
y in Y
by A31; :: thesis: verumassume
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;then Line (a9,b9) c= Y by A2, A8, A13, A26, Th23;

hence y in Y by A27; :: thesis: verum

hence X /\ Y is being_line by A9, A10, XBOOLE_0:def 10; :: thesis: verum