let T be non empty trivial TopSpace; :: thesis: for t being Point of T
for L being Loop of t holds the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))}
let t be Point of T; :: thesis: for L being Loop of t holds the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))}
set E = EqRel (T,t);
let L be Loop of t; :: thesis: the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))}
thus the carrier of (pi_1 (T,t)) c= {(Class ((EqRel (T,t)),L))} :: according to XBOOLE_0:def 10 :: thesis: {(Class ((EqRel (T,t)),L))} c= the carrier of (pi_1 (T,t))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (pi_1 (T,t)) or x in {(Class ((EqRel (T,t)),L))} )
assume x in the carrier of (pi_1 (T,t)) ; :: thesis: x in {(Class ((EqRel (T,t)),L))}
then consider P being Loop of t such that
A1: x = Class ((EqRel (T,t)),P) by TOPALG_1:47;
P = I[01] --> t by TOPREALC:22
.= L by TOPREALC:22 ;
hence x in {(Class ((EqRel (T,t)),L))} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Class ((EqRel (T,t)),L))} or x in the carrier of (pi_1 (T,t)) )
assume x in {(Class ((EqRel (T,t)),L))} ; :: thesis: x in the carrier of (pi_1 (T,t))
then A2: x = Class ((EqRel (T,t)),L) by TARSKI:def 1;
L in Loops t by TOPALG_1:def 1;
then x in Class (EqRel (T,t)) by A2, EQREL_1:def 3;
hence x in the carrier of (pi_1 (T,t)) by TOPALG_1:def 5; :: thesis: verum