let AS be AffinSpace; :: thesis: for x being set holds
( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )
let x be set ; :: thesis: ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )

A1: now :: thesis: ( x in [:(Dir_of_Planes AS),{2}:] implies ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )

assume x in [:(Dir_of_Planes AS),{2}:] ; :: thesis: ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane )
then consider x1, x2 being object such that
A2: x1 in Dir_of_Planes AS and
A3: x2 in {2} and
A4: x = [x1,x2] by ZFMISC_1:def 2;
consider X being Subset of AS such that
A5: x1 = PDir X and
A6: X is being_plane by A2, Th15;
take X = X; :: thesis: ( x = [(PDir X),2] & X is being_plane )
thus x = [(PDir X),2] by A3, A4, A5, TARSKI:def 1; :: thesis: X is being_plane
thus X is being_plane by A6; :: thesis: verum

end;

( ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) implies x in [:(Dir_of_Planes AS),{2}:] ) by Th15, ZFMISC_1:106;
hence ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) ) by A1; :: thesis: verum