let L1 be meet-continuous Semilattice; :: thesis: for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
L2 is meet-continuous
let L2 be non empty reflexive RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L2 is meet-continuous )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: L2 is meet-continuous
hence L2 is up-complete by WAYBEL_8:15; :: according to WAYBEL_2:def 7 :: thesis: L2 is satisfying_MC
let x be Element of L2; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being Element of bool the carrier of L2 holds x "/\" ("\/" (b₁,L2)) = "\/" (({x} "/\" b₁),L2)
let D be non empty directed Subset of L2; :: thesis: x "/\" ("\/" (D,L2)) = "\/" (({x} "/\" D),L2)
reconsider E = D as non empty directed Subset of L1 by A1, WAYBEL_0:3;
reconsider y = x as Element of L1 by A1;
A2: {x} "/\" D = {y} "/\" E by A1, Th11;
reconsider yy = {y} as non empty directed Subset of L1 by WAYBEL_0:5;
A3: ex_sup_of yy "/\" E,L1 by WAYBEL_0:75;
ex_sup_of E,L1 by WAYBEL_0:75;
then sup D = sup E by A1, YELLOW_0:26;
hence x "/\" (sup D) = y "/\" (sup E) by A1, Th9
.= sup ({y} "/\" E) by WAYBEL_2:def 6
.= sup ({x} "/\" D) by A1, A2, A3, YELLOW_0:26 ;
:: thesis: verum