let L be reflexive antisymmetric with_suprema RelStr ; :: thesis: for A being Subset of L holds A c= A "\/" A
let A be Subset of L; :: thesis: A c= A "\/" A
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in A or q in A "\/" A )
assume A1: q in A ; :: thesis: q in A "\/" A
then reconsider A1 = A as non empty Subset of L ;
reconsider q1 = q as Element of A1 by A1;
q1 <= q1 ;
then q1 = q1 "\/" q1 by YELLOW_0:24;
hence q in A "\/" A ; :: thesis: verum