let A be set ; :: thesis: for a, b being Element of holds a "/\" b = a /\ b
let a, b be Element of ; :: thesis: a "/\" b = a /\ b

A1: now

let x, y be Element of ; :: thesis: x "/\" y = x /\ y
reconsider e1 = x as Equivalence_Relation of by MSUALG_7:1;
reconsider e2 = y as Equivalence_Relation of by MSUALG_7:1;
thus x "/\" y = the L_meet of (EqRelLatt A) . e1,e2 by LATTICES:def 2
.= x /\ y by MSUALG_5:def 2 ; :: thesis: verum

end;

reconsider y = b as Element of ;
reconsider x = a as Element of ;
reconsider x = x as Element of ;
reconsider y = y as Element of ;
( % (x % ) = x % & % (y % ) = y % ) ;
hence a "/\" b = x "/\" y by Th7
.= a /\ b by A1 ;
:: thesis: verum
reconsider a1 = a, b1 = b as Element of ;