let L be LATTICE; :: thesis: for a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

let a, b be Element of L; :: thesis: ( L is modular implies subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic )
assume A1: L is modular ; :: thesis: subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
defpred S1[ object , object ] means ( \$2 is Element of L & ( for X, Y being Element of L st \$1 = X & \$2 = Y holds
Y = X "/\" a ) );
A2: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds
ex y being object st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (subrelstr [#b,(a "\/" b)#]) implies ex y being object st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] ) )

assume x in the carrier of (subrelstr [#b,(a "\/" b)#]) ; :: thesis: ex y being object st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )

then A3: x in [#b,(a "\/" b)#] by YELLOW_0:def 15;
then reconsider x1 = x as Element of L ;
take y = a "/\" x1; :: thesis: ( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
x1 <= a "\/" b by ;
then y <= a "/\" (a "\/" b) by YELLOW_5:6;
then A4: y <= a by LATTICE3:18;
b <= x1 by ;
then a "/\" b <= y by YELLOW_5:6;
then y in [#(a "/\" b),a#] by ;
hence y in the carrier of (subrelstr [#(a "/\" b),a#]) by YELLOW_0:def 15; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
consider f being Function of the carrier of (subrelstr [#b,(a "\/" b)#]), the carrier of (subrelstr [#(a "/\" b),a#]) such that
A5: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds
S1[x,f . x] from reconsider f = f as Function of (subrelstr [#b,(a "\/" b)#]),(subrelstr [#(a "/\" b),a#]) ;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
thus f is isomorphic :: thesis: verum
proof
A6: b <= a "\/" b by YELLOW_0:22;
b <= b ;
then b in [#b,(a "\/" b)#] by ;
then reconsider s1 = subrelstr [#b,(b "\/" a)#] as non empty full Sublattice of L by YELLOW_0:def 15;
A7: a "/\" b <= a by YELLOW_0:23;
a "/\" b <= a "/\" b ;
then a "/\" b in [#(a "/\" b),a#] by ;
then reconsider s2 = subrelstr [#(a "/\" b),a#] as non empty full Sublattice of L by YELLOW_0:def 15;
reconsider f1 = f as Function of s1,s2 ;
dom f1 = the carrier of (subrelstr [#b,(a "\/" b)#]) by FUNCT_2:def 1;
then A8: dom f1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;
the carrier of (subrelstr [#(a "/\" b),a#]) c= rng f1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (subrelstr [#(a "/\" b),a#]) or y in rng f1 )
assume y in the carrier of (subrelstr [#(a "/\" b),a#]) ; :: thesis: y in rng f1
then A9: y in [#(a "/\" b),a#] by YELLOW_0:def 15;
then reconsider Y = y as Element of L ;
A10: a "/\" b <= Y by ;
then (a "/\" b) "\/" b <= Y "\/" b by WAYBEL_1:2;
then A11: b <= Y "\/" b by LATTICE3:17;
A12: Y <= a by ;
then Y "\/" b <= a "\/" b by WAYBEL_1:2;
then A13: Y "\/" b in [#b,(a "\/" b)#] by ;
then A14: Y "\/" b in the carrier of (subrelstr [#b,(a "\/" b)#]) by YELLOW_0:def 15;
then reconsider f1yb = f1 . (Y "\/" b) as Element of L by A5;
f1yb = (Y "\/" b) "/\" a by
.= Y "\/" (b "/\" a) by
.= Y by ;
hence y in rng f1 by ; :: thesis: verum
end;
then A15: rng f1 = the carrier of (subrelstr [#(a "/\" b),a#]) ;
A16: for x, y being Element of s1 holds
( x <= y iff f1 . x <= f1 . y )
proof
let x, y be Element of s1; :: thesis: ( x <= y iff f1 . x <= f1 . y )
A17: the carrier of s1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;
then x in [#b,(a "\/" b)#] ;
then reconsider X = x as Element of L ;
y in [#b,(a "\/" b)#] by A17;
then reconsider Y = y as Element of L ;
reconsider f1Y = f1 . Y as Element of L by A5;
reconsider f1X = f1 . X as Element of L by A5;
thus ( x <= y implies f1 . x <= f1 . y ) :: thesis: ( f1 . x <= f1 . y implies x <= y )
proof
assume x <= y ; :: thesis: f1 . x <= f1 . y
then A18: [x,y] in the InternalRel of s1 by ORDERS_2:def 5;
the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13;
then A19: X <= Y by ;
A20: f1Y = Y "/\" a by A5;
f1X = X "/\" a by A5;
then f1X <= f1Y by ;
hence f1 . x <= f1 . y by YELLOW_0:60; :: thesis: verum
end;
thus ( f1 . x <= f1 . y implies x <= y ) :: thesis: verum
proof
assume f1 . x <= f1 . y ; :: thesis: x <= y
then A21: [(f1 . x),(f1 . y)] in the InternalRel of s2 by ORDERS_2:def 5;
the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13;
then A22: f1X <= f1Y by ;
A23: f1Y = Y "/\" a by A5;
A24: b <= X by ;
f1X = X "/\" a by A5;
then b "\/" (a "/\" X) <= b "\/" (a "/\" Y) by ;
then A25: (b "\/" a) "/\" X <= b "\/" (a "/\" Y) by ;
A26: X <= b "\/" a by ;
b <= Y by ;
then (b "\/" a) "/\" X <= (b "\/" a) "/\" Y by ;
then A27: X <= (b "\/" a) "/\" Y by ;
Y <= b "\/" a by ;
then X <= Y by ;
hence x <= y by YELLOW_0:60; :: thesis: verum
end;
end;
f1 is V13()
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in K21(f1) or not x2 in K21(f1) or not f1 . x1 = f1 . x2 or x1 = x2 )
assume that
A28: x1 in dom f1 and
A29: x2 in dom f1 and
A30: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2
reconsider X2 = x2 as Element of L by ;
A31: b <= X2 by ;
reconsider X1 = x1 as Element of L by ;
A32: b <= X1 by ;
reconsider f1X1 = f1 . X1 as Element of L by ;
A33: f1X1 = X1 "/\" a by ;
reconsider f1X2 = f1 . X2 as Element of L by ;
A34: f1X2 = X2 "/\" a by ;
A35: X2 <= a "\/" b by ;
X1 <= a "\/" b by ;
then X1 = (b "\/" a) "/\" X1 by YELLOW_5:10
.= b "\/" (a "/\" X2) by A1, A30, A32, A33, A34
.= (b "\/" a) "/\" X2 by
.= X2 by ;
hence x1 = x2 ; :: thesis: verum
end;
hence f is isomorphic by ; :: thesis: verum
end;