let L be non empty RelStr ; :: thesis: for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds
X1 "\/" X2 c= Y1 "\/" Y2
let X1, X2, Y1, Y2 be Subset of L; :: thesis: ( X1 c= Y1 & X2 c= Y2 implies X1 "\/" X2 c= Y1 "\/" Y2 )
assume A1: ( X1 c= Y1 & X2 c= Y2 ) ; :: thesis: X1 "\/" X2 c= Y1 "\/" Y2
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in X1 "\/" X2 or q in Y1 "\/" Y2 )
assume q in X1 "\/" X2 ; :: thesis: q in Y1 "\/" Y2
then ex x, y being Element of L st
( q = x "\/" y & x in X1 & y in X2 ) ;
hence q in Y1 "\/" Y2 by A1; :: thesis: verum