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 (idsMap 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 (idsMap S) iff x is Ideal of S )

let x be set ; :: thesis: ( x in dom (idsMap S) iff x is Ideal of 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 (idsMap S) by Th53; :: thesis: verum

for x being set holds

( x in dom (idsMap 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 (idsMap S) iff x is Ideal of S )

let x be set ; :: thesis: ( x in dom (idsMap S) iff x is Ideal of S )

hereby :: thesis: ( x is Ideal of S implies x in dom (idsMap S) )

assume
x is Ideal of S
; :: thesis: x in dom (idsMap S)assume
x in dom (idsMap S)
; :: thesis: x is Ideal of S

then x in Ids S by Th53;

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;then x in Ids S by Th53;

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

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 (idsMap S) by Th53; :: thesis: verum