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:26;
( 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, Def2, AFF_1:def 3;
hence Line a,b c= X by A2, A3, A4, Lm5; :: thesis: verum