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

proof

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

now :: thesis: for y being object holds
( ( 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 ) )

let y be object ; :: 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 y9 = y as Element of E ;
y9 is_fixed_under T by A1, 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 A4: ex y9 being Element of E st
( y = y9 & y9 is_fixed_under T ) ;
then S₁[y] ;
hence y in X by A2, A1, A4; :: 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