let L be non empty reflexive transitive with_suprema RelStr ; :: thesis: the carrier of L is Ideal of L
[#] L is Ideal of L ;
hence the carrier of L is Ideal of L ; :: thesis: verum