let L be non empty reflexive transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L
for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
let S be non empty full SubRelStr of L; :: thesis: for x being set holds
( x in dom (supMap S) iff x is Ideal of S )
let x be set ; :: thesis: ( x in dom (supMap S) iff x is Ideal of S )
hereby :: thesis: ( x is Ideal of S implies x in dom (supMap S) )
assume x in dom (supMap S) ; :: thesis: x is Ideal of S
then x in Ids S by Th51;
then x in { X where X is Ideal of S : verum } by WAYBEL_0:def 23;
then ex I being Ideal of S st x = I ;
hence x is Ideal of S ; :: thesis: verum
end;
assume x is Ideal of S ; :: thesis: x in dom (supMap S)
then x in { X where X is Ideal of S : verum } ;
then x in Ids S by WAYBEL_0:def 23;
hence x in dom (supMap S) by Th51; :: thesis: verum