( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E )

proof

assume A1: not E is empty ; :: thesis: { x where x is Element of E : x is_fixed_under T } is Subset of E
defpred S₁[ set ] means for x being Element of E st x = $1 holds
x is_fixed_under T;
consider X being Subset of E such that
A2: for x being set holds
( x in X iff ( x in E & S₁[x] ) ) from SUBSET_1:sch 1();
set Y = { x where x is Element of E : x is_fixed_under T } ;

now

let y be set ; :: thesis: ( ( y in X implies y in { x where x is Element of E : x is_fixed_under T } ) & ( y in { x where x is Element of E : x is_fixed_under T } implies y in X ) )

hereby :: thesis: ( y in { x where x is Element of E : x is_fixed_under T } implies y in X )

assume A3: y in X ; :: thesis: y in { x where x is Element of E : x is_fixed_under T }
then reconsider y' = y as Element of E ;
y' is_fixed_under T by A2, A3;
hence y in { x where x is Element of E : x is_fixed_under T } ; :: thesis: verum

end;

assume y in { x where x is Element of E : x is_fixed_under T } ; :: thesis: y in X
then consider y' being Element of E such that
A4: ( y = y' & y' is_fixed_under T ) ;
( y in E & S₁[y] ) by A1, A4;
hence y in X by A2; :: thesis: verum

end;

hence { x where x is Element of E : x is_fixed_under T } is Subset of E by TARSKI:2; :: thesis: verum

end;

hence ( ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E ) & ( E is empty implies {} E is Subset of E ) & ( for b₁ being Subset of E holds verum ) ) ; :: thesis: verum