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

proof

set Y = { x where x is Element of E : x is_fixed_under T } ;
defpred S₁[ set ] means for x being Element of E st x = $1 holds
x is_fixed_under T;
consider X being Subset of 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

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 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 y' being Element of E st
( y = y' & y' 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 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 is empty implies {} E is Subset of ) & ( for b₁ being Subset of holds verum ) ) ; :: thesis: verum