let AS be AffinSpace; 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; 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; ( 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
; 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
;
contradiction
then consider x being
set such that A11:
x in X /\ Y
and A12:
not
x in Line a,
b
by TARSKI:def 3;
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
set holds
(
y in X iff
y in Y )
proof
let y be
set ;
( y in X iff y in Y )
A15:
now assume A16:
y in Y
;
y in Xnow reconsider b9 =
y as
Element of
AS by A16;
set M =
Line a9,
b9;
A17:
a9 in Line a9,
b9
by AFF_1:26;
A18:
b9 in Line a9,
b9
by AFF_1:26;
assume A19:
y <> x
;
y in Xthen 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 assume
not
Line a9,
b9 // Line a,
b
;
y in Xthen 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:71;
then
Line a9,
b9 c= X
by A1, A7, A12, A14, A24, Th19;
hence
y in X
by A18;
verum end; hence
y in X
by A22;
verum end; hence
y in X
by A11, XBOOLE_0:def 4;
verum end;
now assume A25:
y in X
;
y in Ynow reconsider b9 =
y as
Element of
AS by A25;
set M =
Line a9,
b9;
A26:
a9 in Line a9,
b9
by AFF_1:26;
A27:
b9 in Line a9,
b9
by AFF_1:26;
assume A28:
y <> x
;
y in Ythen 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 assume
not
Line a9,
b9 // Line a,
b
;
y in Ythen 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:71;
then
Line a9,
b9 c= Y
by A2, A8, A12, A13, A33, Th19;
hence
y in Y
by A27;
verum end; hence
y in Y
by A31;
verum end; hence
y in Y
by A11, XBOOLE_0:def 4;
verum end;
hence
(
y in X iff
y in Y )
by A15;
verum
end;
hence
contradiction
by A5, TARSKI:2;
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; verum