let A be set ; :: thesis: for a, b being Element of (EqRelLATT A)
for E1, E2 being Equivalence_Relation of A st a = E1 & b = E2 holds
a "\/" b = E1 "\/" E2
let a, b be Element of (EqRelLATT A); :: thesis: for E1, E2 being Equivalence_Relation of A st a = E1 & b = E2 holds
a "\/" b = E1 "\/" E2
let E1, E2 be Equivalence_Relation of A; :: thesis: ( a = E1 & b = E2 implies a "\/" b = E1 "\/" E2 )
assume A1: ( a = E1 & b = E2 ) ; :: thesis: a "\/" b = E1 "\/" E2
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 Th9
.= the L_join of (EqRelLatt A) . (x,y) by LATTICES:def 1
.= E1 "\/" E2 by A1, MSUALG_5:def 2 ;
:: thesis: verum