let A be set ; :: thesis: for a, b being Element of (EqRelLATT A) holds a "/\" b = a /\ b
let a, b be Element of (EqRelLATT A); :: thesis: a "/\" b = a /\ b
A1: now :: thesis: for x, y being Element of (EqRelLatt A) holds x "/\" y = x /\ y
let x, y be Element of (EqRelLatt A); :: thesis: x "/\" y = x /\ y
reconsider e1 = x as Equivalence_Relation of A by MSUALG_5:21;
reconsider e2 = y as Equivalence_Relation of A by MSUALG_5:21;
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 (LattPOSet (EqRelLatt A)) ;
reconsider x = a as Element of (LattPOSet (EqRelLatt A)) ;
reconsider x = x as Element of (EqRelLatt A) ;
reconsider y = y as Element of (EqRelLatt A) ;
( % (x %) = x % & % (y %) = y % ) ;
hence a "/\" b = x "/\" y by Th7
.= a /\ b by A1 ;
:: thesis: verum