let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_plane holds
for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let X be Subset of AS; :: thesis: ( X is being_plane implies for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) )
assume A1: X is being_plane ; :: thesis: for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let x be set ; :: thesis: ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
A2: now :: thesis: ( x in PDir X implies ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
assume x in PDir X ; :: thesis: ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y )
then [x,X] in PlanesParallelity AS by EQREL_1:19;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: K is being_plane and
A5: M is being_plane and
A6: K '||' M ;
take Y = K; :: thesis: ( x = Y & Y is being_plane & X '||' Y )
X = M by A3, XTUPLE_0:1;
hence ( x = Y & Y is being_plane & X '||' Y ) by A3, A4, A5, A6, AFF_4:58, XTUPLE_0:1; :: thesis: verum
end;
now :: thesis: ( ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) implies x in PDir X )
given Y being Subset of AS such that A7: x = Y and
A8: Y is being_plane and
A9: X '||' Y ; :: thesis: x in PDir X
Y '||' X by A1, A8, A9, AFF_4:58;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_plane & M is being_plane & K '||' M ) } by A1, A8;
hence x in PDir X by A7, EQREL_1:19; :: thesis: verum
end;
hence ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) by A2; :: thesis: verum