let AS be AffinSpace; :: thesis: for a, b being Element of AS
for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds
Line (a,b) c= X
let a, b be Element of AS; :: thesis: for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds
Line (a,b) c= X
let X be Subset of AS; :: thesis: ( X is being_plane & a in X & b in X & a <> b implies Line (a,b) c= X )
assume that
A1: X is being_plane and
A2: ( a in X & b in X ) and
A3: a <> b ; :: thesis: Line (a,b) c= X
set Q = Line (a,b);
A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
( Line (a,b) is being_line & ex K, P being Subset of AS st
( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) ) by A1, A3, AFF_1:def 3;
hence Line (a,b) c= X by A2, A3, A4, Lm5; :: thesis: verum