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 object ; :: 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