let AS be AffinSpace; 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 ; ( 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 ( 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}:]
;
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;
( x = [(PDir X),2] & X is being_plane )thus
x = [(PDir X),2]
by A3, A4, A5, TARSKI:def 1;
X is being_plane thus
X is
being_plane
by A6;
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; verum